$\forall$$T$:Type, $l$:($T$ List), $i$:$\mathbb{Z}$, $j$:\{0..$\parallel$$l$$\parallel^{-}$\}, $x$:$T$.
\\[0ex]$l$[$i$:=$x$][$j$] = if ($j$ =$_{0}$ $i$) then $x$ else $l$[$j$] fi  $\in$ $T$